perm filename YYY[P,JRA]1 blob
sn#082773 filedate 1974-01-21 generic text, type T, neo UTF8
00100
00200 (CSYM AV00)
00300 (THVSETQ (THV ANS) (LIST (LIST (QUOTE THV) (GENSYM))))
00400 (THVSET (CAR (THV ANS)) NIL)
00500
00600
00700 (THVSETQ (THV WF) NIL)
00800 (THVSETQ (THV GCTR) 0)
00900 (THVSETQ (THV ULS) T)
01000 (THVSETQ (THV UF) NIL)
01100 (THVSETQ (THV XN) 0)
01200 (THVSETQ (THV ZN) 0)
01300 (THVSETQ (THV YN) 0)
01400 (THVSETQ (THV COMMENTLIST) NIL)
01500 (THVSETQ (THV PLANL) NIL)
01600 (THVSETQ (THV ASSL) NIL)
01700 (THVSETQ (THV PASSUM) NIL)
01800 (SETQ GTEMP NIL)
01900 (SETQ CT NIL)
02000 (SETQ BTSW NIL)
02100 (THVSETQ (THV DG) NIL)
02200 (SETQ AL NIL)
02300 (SETQ AN 0)
02400 (SETQ SRULES (QUOTE NIL))
02500 (SETQ SSW NIL)
02600 (SETQ FIFOL NIL)
02700 (SETQ LIFOL NIL)
02800 (SETQ SN 0)
02900 (SETQ PN 0)
03000 (SETQ READY NIL)
03100 (SETQ UNCERTLIST NIL)
03200 (THVSETQ (THV DBLITS) NIL)
03300 (THVSETQ (THV ASSERTLITS) NIL)
03400 (THVSETQ (THV WASSERTLITS) NIL)
03500 (SETQ JOINCOND NIL)
03600 (THVSETQ (THV PROCLIST) NIL)
03700 (THVSETQ (THV PROCDATA) NIL)
03800
03900
04000 (THASSERT (ISVAR Z))
04100 (THASSERT (VAR A R))
04200 (THASSERT (VAR B R))
04300 (THASSERT (VUNIFY NIL* NIL* NIL* R))
04400
04500
04600 (THVSETQ (THV UNIFYARGS) NIL)
04700 (THVSETQ (THV UNIFYINST) NIL)
04800
04900 (DEFPROP UNIFYGREMLIN (THERASING (V1 V2 V3) (UNIFY (THV V1) (THV V2) (THV V3) R) (THCOND ((MEMBER (THV UNIFYINST~
05000 ) (THV UNIFYARGS)) (THASSERT (WRONG PATH))))) THEOREM)
05100
05200 (THASSERT UNIFYGREMLIN)
05300
05400 (THVSETQ (THV NUNIFYARGS) NIL)
05500 (THVSETQ (THV NUNIFYINST) NIL)
05600
05700 (DEFPROP NUNIFYGREMLIN (THERASING (V1 V2 V3) (NUNIFY (THV V1) (THV V2) (THV V3) R) (THCOND ((MEMBER (THV NUNIFYI~
05800 NST) (THV NUNIFYARGS)) (THASSERT (WRONG PATH))))) THEOREM)
05900
06000 (THASSERT NUNIFYGREMLIN)
06100
06200 (THVSETQ (THV CUNIFY1ARGS) NIL)
06300 (THVSETQ (THV CUNIFY1INST) NIL)
06400
06500 (DEFPROP CUNIFY1GREMLIN (THERASING (V1 V2 V3 V4) (CUNIFY1 (THV V1) (THV V2) (THV V3) (THV V4) R) (THCOND ((MEMBE~
06600 R (THV CUNIFY1INST) (THV CUNIFY1ARGS)) (THASSERT (WRONG PATH))))) THEOREM)
06700
06800 (THASSERT CUNIFY1GREMLIN)
06900
07000 (THVSETQ (THV NCUNIFY1ARGS) NIL)
07100 (THVSETQ (THV NCUNIFY1INST) NIL)
07200
07300 (DEFPROP NCUNIFY1GREMLIN (THERASING (V1 V2 V3 V4) (NCUNIFY1 (THV V1) (THV V2) (THV V3) (THV V4) R) (THCOND ((MEM~
07400 BER (THV NCUNIFY1INST) (THV NCUNIFY1ARGS)) (THASSERT (WRONG PATH))))) THEOREM)
07500
07600 (THASSERT NCUNIFY1GREMLIN)
07700
07800 (THVSETQ (THV CARGS) NIL)
07900 (THVSETQ (THV CINST) NIL)
08000
08100 (DEFPROP CGREMLIN (THERASING (V1 V2) (C (THV V1) (THV V2) R) (THCOND ((MEMBER (THV CINST) (THV CARGS)) (THASSERT~
08200 (WRONG PATH))))) THEOREM)
08300
08400 (THASSERT CGREMLIN)
08500
08600 (THVSETQ (THV NCARGS) NIL)
08700 (THVSETQ (THV NCINST) NIL)
08800
08900 (DEFPROP NCGREMLIN (THERASING (V1 V2) (NC (THV V1) (THV V2) R) (THCOND ((MEMBER (THV NCINST) (THV NCARGS)) (THAS~
09000 SERT (WRONG PATH))))) THEOREM)
09100
09200 (THASSERT NCGREMLIN)
09300
09400 (THVSETQ (THV VARARGS) NIL)
09500 (THVSETQ (THV VARINST) NIL)
09600
09700 (DEFPROP VARGREMLIN (THERASING (V1) (VAR (THV V1) R) (THCOND ((MEMBER (THV VARINST) (THV VARARGS)) (THASSERT (WR~
09800 ONG PATH))))) THEOREM)
09900
10000 (THASSERT VARGREMLIN)
10100
10200 (THVSETQ (THV NVARARGS) NIL)
10300 (THVSETQ (THV NVARINST) NIL)
10400
10500 (DEFPROP NVARGREMLIN (THERASING (V1) (NVAR (THV V1) R) (THCOND ((MEMBER (THV NVARINST) (THV NVARARGS)) (THASSERT~
10600 (WRONG PATH))))) THEOREM)
10700
10800 (THASSERT NVARGREMLIN)
10900
11000 (THVSETQ (THV VUNIFYARGS) NIL)
11100 (THVSETQ (THV VUNIFYINST) NIL)
11200
11300 (DEFPROP VUNIFYGREMLIN (THERASING (V1 V2 V3) (VUNIFY (THV V1) (THV V2) (THV V3) R) (THCOND ((MEMBER (THV VUNIFYI~
11400 NST) (THV VUNIFYARGS)) (THASSERT (WRONG PATH))))) THEOREM)
11500
11600 (THASSERT VUNIFYGREMLIN)
11700
11800 (THVSETQ (THV NVUNIFYARGS) NIL)
11900 (THVSETQ (THV NVUNIFYINST) NIL)
12000
12100 (DEFPROP NVUNIFYGREMLIN (THERASING (V1 V2 V3) (NVUNIFY (THV V1) (THV V2) (THV V3) R) (THCOND ((MEMBER (THV NVUNI~
12200 FYINST) (THV NVUNIFYARGS)) (THASSERT (WRONG PATH))))) THEOREM)
12300
12400 (THASSERT NVUNIFYGREMLIN)
12500
12600 (THVSETQ (THV =ARGS) NIL)
12700 (THVSETQ (THV =INST) NIL)
12800
12900 (DEFPROP =GREMLIN (THERASING (V1 V2) (= (THV V1) (THV V2) R) (THCOND ((MEMBER (THV =INST) (THV =ARGS)) (THASSERT~
13000 (WRONG PATH))))) THEOREM)
13100
13200 (THASSERT =GREMLIN)
13300
13400 (THVSETQ (THV N=ARGS) NIL)
13500 (THVSETQ (THV N=INST) NIL)
13600
13700 (DEFPROP N=GREMLIN (THERASING (V1 V2) (N= (THV V1) (THV V2) R) (THCOND ((MEMBER (THV N=INST) (THV N=ARGS)) (THAS~
13800 SERT (WRONG PATH))))) THEOREM)
13900
14000 (THASSERT N=GREMLIN)
14100
14200
14300
14400 (SETQ RTTAUNIFY NIL)
14500 (SETQ RFTAUNIFY NIL)
14600 (DEFPROP TAUNIFY
14700 (THCONSE (CGL V11 V10 V9 (LSTTAUNIFY (QUOTE (V11 V10 V9))))
14800 (VUNIFY (THV V9) (THV V10) (THV V11) R)
14900 (THSETQ (THV LCTR) (THV GCTR))
15000 (SETQ THME (ADD1 THME))
15100 (TREEPATH TAUNIFY (VUNIFY (THV V9) (THV V10) (THV V11) R))
15200 (TRACEINFO1)
15300 (THOR T (TRACEINFO2 TAUNIFY))
15400 (COND ((TTYIN) (ADVICESYS)) (T T))
15500 (THCOND ((THASVAL (THV V10)) (EQUAL (THV V10) (THV V10))) (T (THSETQ (THV V10) (THV V10))))
15600 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
15700 (SETQ THMS (ADD1 THMS))
15800 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
15900 THEOREM)
16000
16100
16200 (SETQ RTVARNOT_VARNOT NIL)
16300 (SETQ RFVARNOT_VARNOT NIL)
16400 (DEFPROP VARNOT_VARNOT
16500 (THCONSE (CGL T2 T1 V9 V3 (LSTVARNOT_VARNOT (QUOTE (T2 T1 V9 V3))))
16600 (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R)
16700 (THSETQ (THV LCTR) (THV GCTR))
16800 (SETQ THME (ADD1 THME))
16900 (THUNIQUE LSTVARNOT_VARNOT)
17000 (TREEPATH VARNOT_VARNOT (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R))
17100 (TRACEINFO1)
17200 (THOR T (TRACEINFO2 VARNOT_VARNOT))
17300 (COND ((TTYIN) (ADVICESYS)) (T T))
17400 (THCOND ((THGOAL (NVAR (THV T1) R) (THTBF FILTEROP)) T)
17500 ((THGOAL (VAR (THV T1) R)) (THFAIL))
17600 (T
17700 (UNCERTLIT (LIST (QUOTE NVAR) (THV T1) (QUOTE R))
17800 NIL
17900 (QUOTE (NVAR (THV T1) R))
18000 (QUOTE (VAR (THV T1) R)))))
18100 (CONDSTAT (THV CGL) NIL)
18200 (THCOND ((THAND (THASVAL (THV T1)))
18300 (THSETQ (THV NVARARGS) (CONS (LIST (THV T1)) (THV NVARARGS))))
18400 (T T))
18500 (THCOND ((THGOAL (NVAR (THV T2) R) (THTBF FILTEROP)) T)
18600 ((THGOAL (VAR (THV T2) R)) (THFAIL))
18700 (T
18800 (UNCERTLIT (LIST (QUOTE NVAR) (THV T2) (QUOTE R))
18900 NIL
19000 (QUOTE (NVAR (THV T2) R))
19100 (QUOTE (VAR (THV T2) R)))))
19200 (CONDSTAT (THV CGL) NIL)
19300 (THCOND ((THAND (THASVAL (THV T2)))
19400 (THSETQ (THV NVARARGS) (CONS (LIST (THV T2)) (THV NVARARGS))))
19500 (T T))
19600 (THCOND ((THASVAL (THV T1))
19700 (EQUAL (LIST (QUOTE FL*) (THV T1)) (LIST (QUOTE FL*) (THV T2))))
19800 (T (THSETQ (LIST (QUOTE FL*) (THV T1)) (LIST (QUOTE FL*) (THV T2)))))
19900 (THGOAL (C (THV V3)
20000 (THEV
20100 (LIST (QUOTE COMPOSEL*)
20200 (LIST (QUOTE TERMS*) (THV T1))
20300 (LIST (QUOTE TERMS*) (THV T2))
20400 (THV V9)))
20500 R)
20600 (THTBF FILTEROP))
20700 (THCOND ((THAND (THASVAL (THV V3)))
20800 (THSETQ (THV CARGS)
20900 (CONS (LIST (THV V3)
21000 (LIST (QUOTE COMPOSEL*)
21100 (LIST (QUOTE TERMS*) (THV T1))
21200 (LIST (QUOTE TERMS*) (THV T2))
21300 (THV V9)))
21400 (THV CARGS))))
21500 (T T))
21600 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
21700 (THCOND ((NULL (THV NVARARGS)) T) (T (THSETQ (THV NVARARGS) (CDR (THV NVARARGS)) T T)))
21800 (THCOND ((NULL (THV NVARARGS)) T) (T (THSETQ (THV NVARARGS) (CDR (THV NVARARGS)) T T)))
21900 (THSET (CAR (THV ANS))
22000 (CONS (CONS (QUOTE VARNOT_VARNOT) (LIST (THV V3) (THV V9) (THV T1) (THV T2)))
22100 (EVAL (CAR (THV ANS)))))
22200 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
22300 (SETQ THMS (ADD1 THMS))
22400 (THASSERT (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R))
22500 (THCOND ((THV ULS)
22600 (THSETQ (THV ASSERTLITS)
22700 (CONS (LIST (LIST (QUOTE CUNIFY1)
22800 (THV V3)
22900 (THV V9)
23000 (THV T1)
23100 (THV T2)
23200 (QUOTE R))
23300 (LIST (QUOTE A) (QUOTE A) (QUOTE A) (QUOTE A)))
23400 (THV ASSERTLITS))))
23500 (T
23600 (THSETQ (THV WASSERTLITS)
23700 (CONS (LIST (LIST (QUOTE CUNIFY1)
23800 (THV V3)
23900 (THV V9)
24000 (THV T1)
24100 (THV T2)
24200 (QUOTE R))
24300 (LIST (QUOTE A) (QUOTE A) (QUOTE A) (QUOTE A)))
24400 (THV WASSERTLITS)))))
24500 (PRINT (REVERSE (EVAL (CAR (THV ANS)))))
24600 (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
24700 (COND ((*GREAT (LENGTH GANS) (LENGTH LGANS)) (SETQ LGANS GANS)) (T T))
24800 (THDO (TERPRI))
24900 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
25000 THEOREM)
25100
25200
25300 (SETQ RTVARNOT_VAR NIL)
25400 (SETQ RFVARNOT_VAR NIL)
25500 (DEFPROP VARNOT_VAR
25600 (THCONSE (CGL T2 T1 V9 V3 (LSTVARNOT_VAR (QUOTE (T2 T1 V9 V3))))
25700 (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R)
25800 (THSETQ (THV LCTR) (THV GCTR))
25900 (SETQ THME (ADD1 THME))
26000 (THUNIQUE LSTVARNOT_VAR)
26100 (TREEPATH VARNOT_VAR (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R))
26200 (TRACEINFO1)
26300 (THOR T (TRACEINFO2 VARNOT_VAR))
26400 (COND ((TTYIN) (ADVICESYS)) (T T))
26500 (THNOT (THGOAL (OCCUR (THV T2) (THV T1))))
26600 (THCOND ((THGOAL (VAR (THV T2) R) (THTBF FILTEROP)) T)
26700 ((THGOAL (NVAR (THV T2) R)) (THFAIL))
26800 (T
26900 (UNCERTLIT (LIST (QUOTE VAR) (THV T2) (QUOTE R))
27000 NIL
27100 (QUOTE (VAR (THV T2) R))
27200 (QUOTE (NVAR (THV T2) R)))))
27300 (CONDSTAT (THV CGL) NIL)
27400 (THCOND ((THAND (THASVAL (THV T2)))
27500 (THSETQ (THV VARARGS) (CONS (LIST (THV T2)) (THV VARARGS))))
27600 (T T))
27700 (THCOND ((THGOAL (NVAR (THV T1) R) (THTBF FILTEROP)) T)
27800 ((THGOAL (VAR (THV T1) R)) (THFAIL))
27900 (T
28000 (UNCERTLIT (LIST (QUOTE NVAR) (THV T1) (QUOTE R))
28100 NIL
28200 (QUOTE (NVAR (THV T1) R))
28300 (QUOTE (VAR (THV T1) R)))))
28400 (CONDSTAT (THV CGL) NIL)
28500 (THCOND ((THAND (THASVAL (THV T1)))
28600 (THSETQ (THV NVARARGS) (CONS (LIST (THV T1)) (THV NVARARGS))))
28700 (T T))
28800 (THGOAL (C (THV V3) (THEV (LIST (QUOTE COMPOSE*) (THV T2) (THV T1) (THV V9))) R)
28900 (THTBF FILTEROP))
29000 (THCOND ((THAND (THASVAL (THV V3)))
29100 (THSETQ (THV CARGS)
29200 (CONS (LIST (THV V3) (LIST (QUOTE COMPOSE*) (THV T2) (THV T1) (THV V9)))
29300 (THV CARGS))))
29400 (T T))
29500 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
29600 (THCOND ((NULL (THV NVARARGS)) T) (T (THSETQ (THV NVARARGS) (CDR (THV NVARARGS)) T T)))
29700 (THCOND ((NULL (THV VARARGS)) T) (T (THSETQ (THV VARARGS) (CDR (THV VARARGS)) T T)))
29800 (THSET (CAR (THV ANS))
29900 (CONS (CONS (QUOTE VARNOT_VAR) (LIST (THV V3) (THV V9) (THV T1) (THV T2)))
30000 (EVAL (CAR (THV ANS)))))
30100 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
30200 (SETQ THMS (ADD1 THMS))
30300 (THASSERT (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R))
30400 (THCOND ((THV ULS)
30500 (THSETQ (THV ASSERTLITS)
30600 (CONS (LIST (LIST (QUOTE CUNIFY1)
30700 (THV V3)
30800 (THV V9)
30900 (THV T1)
31000 (THV T2)
31100 (QUOTE R))
31200 (LIST (QUOTE A) (QUOTE A) (QUOTE A) (QUOTE A)))
31300 (THV ASSERTLITS))))
31400 (T
31500 (THSETQ (THV WASSERTLITS)
31600 (CONS (LIST (LIST (QUOTE CUNIFY1)
31700 (THV V3)
31800 (THV V9)
31900 (THV T1)
32000 (THV T2)
32100 (QUOTE R))
32200 (LIST (QUOTE A) (QUOTE A) (QUOTE A) (QUOTE A)))
32300 (THV WASSERTLITS)))))
32400 (PRINT (REVERSE (EVAL (CAR (THV ANS)))))
32500 (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
32600 (COND ((*GREAT (LENGTH GANS) (LENGTH LGANS)) (SETQ LGANS GANS)) (T T))
32700 (THDO (TERPRI))
32800 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
32900 THEOREM)
33000
33100
33200 (SETQ RTVAR_VARNOT NIL)
33300 (SETQ RFVAR_VARNOT NIL)
33400 (DEFPROP VAR_VARNOT
33500 (THCONSE (CGL T2 T1 V9 V3 (LSTVAR_VARNOT (QUOTE (T2 T1 V9 V3))))
33600 (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R)
33700 (THSETQ (THV LCTR) (THV GCTR))
33800 (SETQ THME (ADD1 THME))
33900 (THUNIQUE LSTVAR_VARNOT)
34000 (TREEPATH VAR_VARNOT (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R))
34100 (TRACEINFO1)
34200 (THOR T (TRACEINFO2 VAR_VARNOT))
34300 (COND ((TTYIN) (ADVICESYS)) (T T))
34400 (THNOT (THGOAL (OCCUR (THV T1) (THV T2))))
34500 (THCOND ((THGOAL (VAR (THV T1) R) (THTBF FILTEROP)) T)
34600 ((THGOAL (NVAR (THV T1) R)) (THFAIL))
34700 (T
34800 (UNCERTLIT (LIST (QUOTE VAR) (THV T1) (QUOTE R))
34900 NIL
35000 (QUOTE (VAR (THV T1) R))
35100 (QUOTE (NVAR (THV T1) R)))))
35200 (CONDSTAT (THV CGL) NIL)
35300 (THCOND ((THAND (THASVAL (THV T1)))
35400 (THSETQ (THV VARARGS) (CONS (LIST (THV T1)) (THV VARARGS))))
35500 (T T))
35600 (THCOND ((THGOAL (NVAR (THV T2) R) (THTBF FILTEROP)) T)
35700 ((THGOAL (VAR (THV T2) R)) (THFAIL))
35800 (T
35900 (UNCERTLIT (LIST (QUOTE NVAR) (THV T2) (QUOTE R))
36000 NIL
36100 (QUOTE (NVAR (THV T2) R))
36200 (QUOTE (VAR (THV T2) R)))))
36300 (CONDSTAT (THV CGL) NIL)
36400 (THCOND ((THAND (THASVAL (THV T2)))
36500 (THSETQ (THV NVARARGS) (CONS (LIST (THV T2)) (THV NVARARGS))))
36600 (T T))
36700 (THGOAL (C (THV V3) (THEV (LIST (QUOTE COMPOSE*) (THV T1) (THV T2) (THV V9))) R)
36800 (THTBF FILTEROP))
36900 (THCOND ((THAND (THASVAL (THV V3)))
37000 (THSETQ (THV CARGS)
37100 (CONS (LIST (THV V3) (LIST (QUOTE COMPOSE*) (THV T1) (THV T2) (THV V9)))
37200 (THV CARGS))))
37300 (T T))
37400 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
37500 (THCOND ((NULL (THV NVARARGS)) T) (T (THSETQ (THV NVARARGS) (CDR (THV NVARARGS)) T T)))
37600 (THCOND ((NULL (THV VARARGS)) T) (T (THSETQ (THV VARARGS) (CDR (THV VARARGS)) T T)))
37700 (THSET (CAR (THV ANS))
37800 (CONS (CONS (QUOTE VAR_VARNOT) (LIST (THV V3) (THV V9) (THV T1) (THV T2)))
37900 (EVAL (CAR (THV ANS)))))
38000 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
38100 (SETQ THMS (ADD1 THMS))
38200 (THASSERT (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R))
38300 (THCOND ((THV ULS)
38400 (THSETQ (THV ASSERTLITS)
38500 (CONS (LIST (LIST (QUOTE CUNIFY1)
38600 (THV V3)
38700 (THV V9)
38800 (THV T1)
38900 (THV T2)
39000 (QUOTE R))
39100 (LIST (QUOTE A) (QUOTE A) (QUOTE A) (QUOTE A)))
39200 (THV ASSERTLITS))))
39300 (T
39400 (THSETQ (THV WASSERTLITS)
39500 (CONS (LIST (LIST (QUOTE CUNIFY1)
39600 (THV V3)
39700 (THV V9)
39800 (THV T1)
39900 (THV T2)
40000 (QUOTE R))
40100 (LIST (QUOTE A) (QUOTE A) (QUOTE A) (QUOTE A)))
40200 (THV WASSERTLITS)))))
40300 (PRINT (REVERSE (EVAL (CAR (THV ANS)))))
40400 (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
40500 (COND ((*GREAT (LENGTH GANS) (LENGTH LGANS)) (SETQ LGANS GANS)) (T T))
40600 (THDO (TERPRI))
40700 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
40800 THEOREM)
40900
41000
41100 (SETQ RTVARVAR NIL)
41200 (SETQ RFVARVAR NIL)
41300 (DEFPROP VARVAR
41400 (THCONSE (CGL T2 T1 V9 V3 (LSTVARVAR (QUOTE (T2 T1 V9 V3))))
41500 (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R)
41600 (THSETQ (THV LCTR) (THV GCTR))
41700 (SETQ THME (ADD1 THME))
41800 (THUNIQUE LSTVARVAR)
41900 (TREEPATH VARVAR (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R))
42000 (TRACEINFO1)
42100 (THOR T (TRACEINFO2 VARVAR))
42200 (COND ((TTYIN) (ADVICESYS)) (T T))
42300 (THCOND ((THGOAL (VAR (THV T1) R) (THTBF FILTEROP)) T)
42400 ((THGOAL (NVAR (THV T1) R)) (THFAIL))
42500 (T
42600 (UNCERTLIT (LIST (QUOTE VAR) (THV T1) (QUOTE R))
42700 NIL
42800 (QUOTE (VAR (THV T1) R))
42900 (QUOTE (NVAR (THV T1) R)))))
43000 (CONDSTAT (THV CGL) NIL)
43100 (THCOND ((THAND (THASVAL (THV T1)))
43200 (THSETQ (THV VARARGS) (CONS (LIST (THV T1)) (THV VARARGS))))
43300 (T T))
43400 (THCOND ((THGOAL (VAR (THV T2) R) (THTBF FILTEROP)) T)
43500 ((THGOAL (NVAR (THV T2) R)) (THFAIL))
43600 (T
43700 (UNCERTLIT (LIST (QUOTE VAR) (THV T2) (QUOTE R))
43800 NIL
43900 (QUOTE (VAR (THV T2) R))
44000 (QUOTE (NVAR (THV T2) R)))))
44100 (CONDSTAT (THV CGL) NIL)
44200 (THCOND ((THAND (THASVAL (THV T2)))
44300 (THSETQ (THV VARARGS) (CONS (LIST (THV T2)) (THV VARARGS))))
44400 (T T))
44500 (THGOAL (C (THV V3) (THEV (LIST (QUOTE COMPOSE*) (THV T1) (THV T2) (THV V9))) R)
44600 (THTBF FILTEROP))
44700 (THCOND ((THAND (THASVAL (THV V3)))
44800 (THSETQ (THV CARGS)
44900 (CONS (LIST (THV V3) (LIST (QUOTE COMPOSE*) (THV T1) (THV T2) (THV V9)))
45000 (THV CARGS))))
45100 (T T))
45200 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
45300 (THCOND ((NULL (THV VARARGS)) T) (T (THSETQ (THV VARARGS) (CDR (THV VARARGS)) T T)))
45400 (THCOND ((NULL (THV VARARGS)) T) (T (THSETQ (THV VARARGS) (CDR (THV VARARGS)) T T)))
45500 (THSET (CAR (THV ANS))
45600 (CONS (CONS (QUOTE VARVAR) (LIST (THV V3) (THV V9) (THV T1) (THV T2)))
45700 (EVAL (CAR (THV ANS)))))
45800 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
45900 (SETQ THMS (ADD1 THMS))
46000 (THASSERT (CUNIFY1 (THV V3) (THV V9) (THV T1) (THV T2) R))
46100 (THCOND ((THV ULS)
46200 (THSETQ (THV ASSERTLITS)
46300 (CONS (LIST (LIST (QUOTE CUNIFY1)
46400 (THV V3)
46500 (THV V9)
46600 (THV T1)
46700 (THV T2)
46800 (QUOTE R))
46900 (LIST (QUOTE A) (QUOTE A) (QUOTE A) (QUOTE A)))
47000 (THV ASSERTLITS))))
47100 (T
47200 (THSETQ (THV WASSERTLITS)
47300 (CONS (LIST (LIST (QUOTE CUNIFY1)
47400 (THV V3)
47500 (THV V9)
47600 (THV T1)
47700 (THV T2)
47800 (QUOTE R))
47900 (LIST (QUOTE A) (QUOTE A) (QUOTE A) (QUOTE A)))
48000 (THV WASSERTLITS)))))
48100 (PRINT (REVERSE (EVAL (CAR (THV ANS)))))
48200 (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
48300 (COND ((*GREAT (LENGTH GANS) (LENGTH LGANS)) (SETQ LGANS GANS)) (T T))
48400 (THDO (TERPRI))
48500 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
48600 THEOREM)
48700
48800
48900 (SETQ RTTUNIFY NIL)
49000 (SETQ RFTUNIFY NIL)
49100 (DEFPROP TUNIFY
49200 (THCONSE (V15 V14
49300 V11
49400 V10
49500 V9
49600 V3
49700 V2
49800 V1
49900 V6
50000 V5
50100 V4
50200 V13
50300 V12
50400 V8
50500 V7
50600 FT
50700 NT
50800 CGL
50900 LCTR
51000 LWF
51100 LUF
51200 PS
51300 PB
51400 BP
51500 SASSERTLITS
51600 INVAR1
51700 INVAR2
51800 CTST)
51900 (UNIFY (THV V3) (THV V1) (THV V2) R)
52000 (THSETQ (THV LCTR) (THV GCTR))
52100 (SETQ THME (ADD1 THME))
52200 (TREEPATH TUNIFY (UNIFY (THV V3) (THV V1) (THV V2) R))
52300 (TRACEINFO1)
52400 (THOR T (TRACEINFO2 TUNIFY))
52500 (COND ((TTYIN) (ADVICESYS)) (T T))
52600 (THSETQ (THV LWF) NIL T T)
52700 (THCOND ((NOT (THV WF)) (THSETQ (THV LWF) T)) (T T))
52800 (THSETQ (THV WF) T)
52900 (THSETQ (THV LUF) NIL T T)
53000 (THSETQ (THV PS) (EVAL (CAR (THV ANS))) T T)
53100 (THSET (CAR (THV ANS)) NIL)
53200 (NEWVAR (THV V7))
53300 (NEWVAR (THV V8))
53400 (NEWVAR (THV V12))
53500 (NEWVAR (THV V13))
53600 (THGOAL (VUNIFY (THV V4) (THV V5) (THV V6) R) (THTBF FILTEROP))
53700 (THCOND
53800 ((THAND (THASVAL (THV V6)) (THASVAL (THV V5)) (THASVAL (THV V4)))
53900 (THSETQ (THV VUNIFYARGS) (CONS (LIST (THV V4) (THV V5) (THV V6)) (THV VUNIFYARGS))))
54000 (T T))
54100 (THGOAL (C (THV V12) (THV V1) R) (THTBF FILTEROP))
54200 (THCOND ((THAND (THASVAL (THV V1)) (THASVAL (THV V12)))
54300 (THSETQ (THV CARGS) (CONS (LIST (THV V12) (THV V1)) (THV CARGS))))
54400 (T T))
54500 (THGOAL (C (THV V13) (THV V2) R) (THTBF FILTEROP))
54600 (THCOND ((THAND (THASVAL (THV V2)) (THASVAL (THV V13)))
54700 (THSETQ (THV CARGS) (CONS (LIST (THV V13) (THV V2)) (THV CARGS))))
54800 (T T))
54900 (THGOAL (C (THV V3) (THV V4) R) (THTBF FILTEROP))
55000 (THCOND ((THAND (THASVAL (THV V4)) (THASVAL (THV V3)))
55100 (THSETQ (THV CARGS) (CONS (LIST (THV V3) (THV V4)) (THV CARGS))))
55200 (T T))
55300 (THGOAL (C (THV V7) (THV V5) R) (THTBF FILTEROP))
55400 (THCOND ((THAND (THASVAL (THV V5)) (THASVAL (THV V7)))
55500 (THSETQ (THV CARGS) (CONS (LIST (THV V7) (THV V5)) (THV CARGS))))
55600 (T T))
55700 (THGOAL (C (THV V8) (THV V6) R) (THTBF FILTEROP))
55800 (THCOND ((THAND (THASVAL (THV V6)) (THASVAL (THV V8)))
55900 (THSETQ (THV CARGS) (CONS (LIST (THV V8) (THV V6)) (THV CARGS))))
56000 (T T))
56100 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
56200 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
56300 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
56400 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
56500 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
56600 (THCOND ((NULL (THV VUNIFYARGS)) T)
56700 (T (THSETQ (THV VUNIFYARGS) (CDR (THV VUNIFYARGS)) T T)))
56800 (THSETQ (THV BP) (EVAL (CAR (THV ANS))) T T)
56900 (THSET (CAR (THV ANS)) NIL)
57000 (THOR T (THFAIL THEOREM))
57100 REP
57200 (THGOAL (C (THV V3) (THV V9) R) (THTBF FILTERAX))
57300 (THGOAL (C (THV V7) (THV V10) R) (THTBF FILTERAX))
57400 (THGOAL (C (THV V8) (THV V11) R) (THTBF FILTERAX))
57500 (THGOAL (C (THV V12) (THV V14) R) (THTBF FILTERAX))
57600 (THGOAL (C (THV V13) (THV V15) R) (THTBF FILTERAX))
57700 (THGOAL (VUNIFY (THV V9) (THV V10) (THV V11) R) (THTBF FILTERAX))
57800 (THSETQ (THV INVAR1)
57900 (LIST (SIMPLE (LIST (QUOTE VUNIFY) (THV V9) (THV V10) (THV V11) (QUOTE R)))
58000 (SIMPLE (LIST (QUOTE C) (THV V13) (THV V15) (QUOTE R)))
58100 (SIMPLE (LIST (QUOTE C) (THV V12) (THV V14) (QUOTE R)))
58200 (SIMPLE (LIST (QUOTE C) (THV V8) (THV V11) (QUOTE R)))
58300 (SIMPLE (LIST (QUOTE C) (THV V7) (THV V10) (QUOTE R)))
58400 (SIMPLE (LIST (QUOTE C) (THV V3) (THV V9) (QUOTE R))))
58500 T
58600 T)
58700 (THSETQ (THV CTST) (LIST (QUOTE =) (THV V14) (THV NIL*)))
58800 (THOR T (THFAIL THEOREM))
58900 (THSETQ (THV SASSERTLITS) (THV ASSERTLITS) T T)
59000 (THGOAL (CUNIFY1 (THV V3)
59100 (THV V9)
59200 (THEV (LIST (QUOTE SUBST*) (THV V9) (LIST (QUOTE CAR*) (THV V14))))
59300 (THEV (LIST (QUOTE SUBST*) (THV V9) (LIST (QUOTE CAR*) (THV V15))))
59400 R)
59500 (THTBF FILTEROP))
59600 (THCOND
59700 ((THAND (THASVAL (THV V9)) (THASVAL (THV V3)))
59800 (THSETQ (THV CUNIFY1ARGS)
59900 (CONS (LIST (THV V3)
60000 (THV V9)
60100 (LIST (QUOTE SUBST*) (THV V9) (LIST (QUOTE CAR*) (THV V14)))
60200 (LIST (QUOTE SUBST*) (THV V9) (LIST (QUOTE CAR*) (THV V15))))
60300 (THV CUNIFY1ARGS))))
60400 (T T))
60500 (THGOAL (C (THV V7) (THEV (LIST (QUOTE CONS*) (THV V10) (LIST (QUOTE CAR*) (THV V14)))) R)
60600 (THTBF FILTEROP))
60700 (THCOND ((THAND (THASVAL (THV V7)))
60800 (THSETQ (THV CARGS)
60900 (CONS (LIST (THV V7)
61000 (LIST (QUOTE CONS*) (THV V10) (LIST (QUOTE CAR*) (THV V14))))
61100 (THV CARGS))))
61200 (T T))
61300 (THGOAL (C (THV V8) (THEV (LIST (QUOTE CONS*) (THV V11) (LIST (QUOTE CAR*) (THV V15)))) R)
61400 (THTBF FILTEROP))
61500 (THCOND ((THAND (THASVAL (THV V8)))
61600 (THSETQ (THV CARGS)
61700 (CONS (LIST (THV V8)
61800 (LIST (QUOTE CONS*) (THV V11) (LIST (QUOTE CAR*) (THV V15))))
61900 (THV CARGS))))
62000 (T T))
62100 (THGOAL (C (THV V12) (THEV (LIST (QUOTE CDR*) (THV V14))) R) (THTBF FILTEROP))
62200 (THCOND ((THAND (THASVAL (THV V12)))
62300 (THSETQ (THV CARGS)
62400 (CONS (LIST (THV V12) (LIST (QUOTE CDR*) (THV V14))) (THV CARGS))))
62500 (T T))
62600 (THGOAL (C (THV V13) (THEV (LIST (QUOTE CDR*) (THV V15))) R) (THTBF FILTEROP))
62700 (THCOND ((THAND (THASVAL (THV V13)))
62800 (THSETQ (THV CARGS)
62900 (CONS (LIST (THV V13) (LIST (QUOTE CDR*) (THV V15))) (THV CARGS))))
63000 (T T))
63100 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
63200 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
63300 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
63400 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
63500 (THCOND ((NULL (THV CUNIFY1ARGS)) T)
63600 (T (THSETQ (THV CUNIFY1ARGS) (CDR (THV CUNIFY1ARGS)) T T)))
63700 (THSETQ (THV V15) (QUOTE THUNASSIGNED))
63800 (THSETQ (THV V14) (QUOTE THUNASSIGNED))
63900 (THSETQ (THV V11) (QUOTE THUNASSIGNED))
64000 (THSETQ (THV V10) (QUOTE THUNASSIGNED))
64100 (THSETQ (THV V9) (QUOTE THUNASSIGNED))
64200 (THGOAL (C (THV V3) (THV V9) R) (THTBF FILTERAX))
64300 (THGOAL (C (THV V7) (THV V10) R) (THTBF FILTERAX))
64400 (THGOAL (C (THV V8) (THV V11) R) (THTBF FILTERAX))
64500 (THGOAL (C (THV V12) (THV V14) R) (THTBF FILTERAX))
64600 (THGOAL (C (THV V13) (THV V15) R) (THTBF FILTERAX))
64700 (THGOAL (VUNIFY (THV V9) (THV V10) (THV V11) R) (THTBF FILTERAX))
64800 (THCOND ((NOT (THASVAL (THV V15))) (THSETQ (THV V15) (QUOTE ##))) (T T))
64900 (THCOND ((NOT (THASVAL (THV V14))) (THSETQ (THV V14) (QUOTE ##))) (T T))
65000 (THCOND ((NOT (THASVAL (THV V11))) (THSETQ (THV V11) (QUOTE ##))) (T T))
65100 (THCOND ((NOT (THASVAL (THV V10))) (THSETQ (THV V10) (QUOTE ##))) (T T))
65200 (THCOND ((NOT (THASVAL (THV V9))) (THSETQ (THV V9) (QUOTE ##))) (T T))
65300 (THSETQ (THV PB) (EVAL (CAR (THV ANS))) T T)
65400 (THSETQ (THV INVAR2)
65500 (LIST (SIMPLE (LIST (QUOTE VUNIFY) (THV V9) (THV V10) (THV V11) (QUOTE R)))
65600 (SIMPLE (LIST (QUOTE C) (THV V13) (THV V15) (QUOTE R)))
65700 (SIMPLE (LIST (QUOTE C) (THV V12) (THV V14) (QUOTE R)))
65800 (SIMPLE (LIST (QUOTE C) (THV V8) (THV V11) (QUOTE R)))
65900 (SIMPLE (LIST (QUOTE C) (THV V7) (THV V10) (QUOTE R)))
66000 (SIMPLE (LIST (QUOTE C) (THV V3) (THV V9) (QUOTE R))))
66100 T
66200 T)
66300 (THCOND ((THASVAL (THV FT))
66400 (THSETQ (THV NT)
66500 (COMPCHANGES (THV INVAR1)
66600 (THV INVAR2)
66700 (INCRELIT (THV SASSERTLITS) (REVERSE (THV ASSERTLITS))))))
66800 (T
66900 (THSETQ (THV FT)
67000 (COMPCHANGES (THV INVAR1)
67100 (THV INVAR2)
67200 (INCRELIT (THV SASSERTLITS) (REVERSE (THV ASSERTLITS)))))))
67300 (THCOND ((AND (NOT (THASVAL (THV NT))) (AMBIG (THV FT))) (THSETQ (THV V15)
67400 (QUOTE THUNASSIGNED))
67500 (THSETQ (THV V14)
67600 (QUOTE THUNASSIGNED))
67700 (THSETQ (THV V11)
67800 (QUOTE THUNASSIGNED))
67900 (THSETQ (THV V10)
68000 (QUOTE THUNASSIGNED))
68100 (THSETQ (THV V9)
68200 (QUOTE THUNASSIGNED))
68300 (THSET (CAR (THV ANS)) NIL)
68400 (THGO REP))
68500 (T T))
68600 (SETQ GTEMP
68700 (WHILASSEM (THV BP)
68800 (THV PB)
68900 (COND ((THASVAL (THV NT)) (THV NT)) (T (THV FT)))
69000 (THV CTST)))
69100 (THSETQ (THV PB) GTEMP T T)
69200 (THSET (CAR (THV ANS)) (APPEND (THV PB) (THV PS)))
69300 (THASSERT (UNIFY (THV V3) (THV V1) (THV V2) R))
69400 (THCOND ((THV ULS)
69500 (THSETQ (THV ASSERTLITS)
69600 (CONS (LIST (LIST (QUOTE UNIFY) (THV V3) (THV V1) (THV V2) (QUOTE R))
69700 (LIST (QUOTE A) (QUOTE A) (QUOTE A)))
69800 (THV ASSERTLITS))))
69900 (T
70000 (THSETQ (THV WASSERTLITS)
70100 (CONS (LIST (LIST (QUOTE UNIFY) (THV V3) (THV V1) (THV V2) (QUOTE R))
70200 (LIST (QUOTE A) (QUOTE A) (QUOTE A)))
70300 (THV WASSERTLITS)))))
70400 (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
70500 (THCOND ((THV LWF) (THSETQ (THV WF) NIL T T)
70600 (THSETQ (THV BT) NIL T T)
70700 (SETQ GANS (REMBT GANS)))
70800 (T T))
70900 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
71000 (THCOND ((THV LUF) (THSETQ (THV UF) NIL T T) (THSETQ (THV ULS) T)) (T T))
71100 (THCOND ((THV ULS)
71200 (THSETQ (THV ASSERTLITS)
71300 (CONS (LIST (LIST (QUOTE UNIFY) (THV V3) (THV V1) (THV V2) (QUOTE R))
71400 (LIST (QUOTE A) (QUOTE A) (QUOTE A)))
71500 (THV ASSERTLITS))))
71600 (T
71700 (THSETQ (THV WASSERTLITS)
71800 (CONS (LIST (LIST (QUOTE UNIFY) (THV V3) (THV V1) (THV V2) (QUOTE R))
71900 (LIST (QUOTE A) (QUOTE A) (QUOTE A)))
72000 (THV WASSERTLITS)))))
72100 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
72200 THEOREM)
72300
72400
72500 (SETQ RT← NIL)
72600 (SETQ RF← NIL)
72700 (DEFPROP ←
72800 (THCONSE (CGL A1 V1 D1 (LST← (QUOTE (A1 V1))))
72900 (C (THV V1) (THV A1) R)
73000 (THSETQ (THV LCTR) (THV GCTR))
73100 (SETQ THME (ADD1 THME))
73200 (THUNIQUE LST←)
73300 (TREEPATH ← (C (THV V1) (THV A1) R))
73400 (TRACEINFO1)
73500 (THOR T (TRACEINFO2 ←))
73600 (COND ((TTYIN) (ADVICESYS)) (T T))
73700 (THGOAL (ISVAR (THV V1)))
73800 (THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THSETQ (THV CINST) (LIST (THV V1) (THV D1))))
73900 (T T))
74000 (THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THERASE (C (THV V1) (THV D1) R) (THTBF THTRUE)))
74100 (T T))
74200 (THCOND ((THERASE (WRONG PATH)) (THFAIL THEOREM)) (T T))
74300 (THSET (CAR (THV ANS))
74400 (CONS (CONS (QUOTE ←) (LIST (THV V1) (THV A1))) (EVAL (CAR (THV ANS)))))
74500 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
74600 (SETQ THMS (ADD1 THMS))
74700 (THASSERT (C (THV V1) (THV A1) R))
74800 (THCOND ((THV ULS)
74900 (THSETQ (THV ASSERTLITS)
75000 (CONS (LIST (LIST (QUOTE C) (THV V1) (THV A1) (QUOTE R))
75100 (LIST (QUOTE A) (QUOTE A)))
75200 (THV ASSERTLITS))))
75300 (T
75400 (THSETQ (THV WASSERTLITS)
75500 (CONS (LIST (LIST (QUOTE C) (THV V1) (THV A1) (QUOTE R))
75600 (LIST (QUOTE A) (QUOTE A)))
75700 (THV WASSERTLITS)))))
75800 (PRINT (REVERSE (EVAL (CAR (THV ANS)))))
75900 (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
76000 (COND ((*GREAT (LENGTH GANS) (LENGTH LGANS)) (SETQ LGANS GANS)) (T T))
76100 (THDO (TERPRI))
76200 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
76300 THEOREM)
76400
76500
76600 (THASSERT ←)
76700
76800
76900 (THASSERT TUNIFY)
77000
77100
77200 (THASSERT VARVAR)
77300
77400
77500 (THASSERT VAR_VARNOT)
77600
77700
77800 (THASSERT VARNOT_VAR)
77900
78000
78100 (THASSERT VARNOT_VARNOT)
78200
78300
78400 (THASSERT TAUNIFY)
78500 (DEFPROP RESTOREPROP
78600 (LAMBDA NIL
78700 (PROG NIL
78800 (SETQ STAT T)
78900 (SETQ FUNDEFLIST (QUOTE NIL))
79000 (PUTPROP (QUOTE UNIFY) T (QUOTE DEF))
79100 (PUTPROP (QUOTE UNIFY) (QUOTE NIL) (QUOTE UNIQ))
79200 (PUTPROP (QUOTE UNIFY) (QUOTE NIL) (QUOTE UNCERT))
79300 (PUTPROP (QUOTE UNIFY) (QUOTE NIL) (QUOTE PARTIAL))
79400 (PUTPROP (QUOTE UNIFY) (QUOTE T) (QUOTE FLUENT))
79500 (PUTPROP (QUOTE VUNIFY) T (QUOTE DEF))
79600 (PUTPROP (QUOTE VUNIFY) (QUOTE NIL) (QUOTE UNIQ))
79700 (PUTPROP (QUOTE VUNIFY) (QUOTE NIL) (QUOTE UNCERT))
79800 (PUTPROP (QUOTE VUNIFY) (QUOTE NIL) (QUOTE PARTIAL))
79900 (PUTPROP (QUOTE VUNIFY) (QUOTE T) (QUOTE FLUENT))
80000 (PUTPROP (QUOTE CUNIFY1) T (QUOTE DEF))
80100 (PUTPROP (QUOTE CUNIFY1) (QUOTE NIL) (QUOTE UNIQ))
80200 (PUTPROP (QUOTE CUNIFY1) (QUOTE NIL) (QUOTE UNCERT))
80300 (PUTPROP (QUOTE CUNIFY1) (QUOTE NIL) (QUOTE PARTIAL))
80400 (PUTPROP (QUOTE CUNIFY1) (QUOTE T) (QUOTE FLUENT))
80500 (PUTPROP (QUOTE CUNIFY) T (QUOTE DEF))
80600 (PUTPROP (QUOTE CUNIFY) (QUOTE NIL) (QUOTE UNIQ))
80700 (PUTPROP (QUOTE CUNIFY) (QUOTE NIL) (QUOTE UNCERT))
80800 (PUTPROP (QUOTE CUNIFY) (QUOTE NIL) (QUOTE PARTIAL))
80900 (PUTPROP (QUOTE CUNIFY) (QUOTE T) (QUOTE FLUENT))
81000 (PUTPROP (QUOTE =) T (QUOTE DEF))
81100 (PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE UNIQ))
81200 (PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE UNCERT))
81300 (PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE PARTIAL))
81400 (PUTPROP (QUOTE =) (QUOTE T) (QUOTE FLUENT))
81500 (PUTPROP (QUOTE VAR) T (QUOTE DEF))
81600 (PUTPROP (QUOTE VAR) (QUOTE NIL) (QUOTE UNIQ))
81700 (PUTPROP (QUOTE VAR) (QUOTE NIL) (QUOTE UNCERT))
81800 (PUTPROP (QUOTE VAR) (QUOTE T) (QUOTE PARTIAL))
81900 (PUTPROP (QUOTE VAR) (QUOTE T) (QUOTE FLUENT))
82000 (PUTPROP (QUOTE C) T (QUOTE DEF))
82100 (PUTPROP (QUOTE C) (QUOTE (X *)) (QUOTE UNIQ))
82200 (PUTPROP (QUOTE C) (QUOTE NIL) (QUOTE UNCERT))
82300 (PUTPROP (QUOTE C) (QUOTE NIL) (QUOTE PARTIAL))
82400 (PUTPROP (QUOTE C) (QUOTE T) (QUOTE FLUENT))
82500 (PUTPROP (QUOTE TAUNIFY) (QUOTE NIL) (QUOTE INEQ))
82600 (PUTPROP (QUOTE TAUNIFY) (QUOTE T) (QUOTE REC))
82700 (PUTPROP (QUOTE TAUNIFY) (QUOTE NIL) (QUOTE ASSUM))
82800 (PUTPROP (QUOTE TAUNIFY) (QUOTE NIL) (QUOTE ARG))
82900 (PUTPROP (QUOTE TAUNIFY) T (QUOTE AX))
83000 (PUTPROP (QUOTE VARNOT_VARNOT) (QUOTE NIL) (QUOTE INEQ))
83100 (PUTPROP (QUOTE VARNOT_VARNOT) (QUOTE NIL) (QUOTE REC))
83200 (PUTPROP (QUOTE VARNOT_VARNOT) (QUOTE NIL) (QUOTE ASSUM))
83300 (PUTPROP (QUOTE VARNOT_VARNOT) (QUOTE (V3 V9 T1 T2)) (QUOTE ARG))
83400 (PUTPROP (QUOTE VARNOT_VARNOT) T (QUOTE OP))
83500 (PUTPROP (QUOTE VARNOT_VAR) (QUOTE NIL) (QUOTE INEQ))
83600 (PUTPROP (QUOTE VARNOT_VAR) (QUOTE NIL) (QUOTE REC))
83700 (PUTPROP (QUOTE VARNOT_VAR) (QUOTE NIL) (QUOTE ASSUM))
83800 (PUTPROP (QUOTE VARNOT_VAR) (QUOTE (V3 V9 T1 T2)) (QUOTE ARG))
83900 (PUTPROP (QUOTE VARNOT_VAR) T (QUOTE OP))
84000 (PUTPROP (QUOTE VAR_VARNOT) (QUOTE NIL) (QUOTE INEQ))
84100 (PUTPROP (QUOTE VAR_VARNOT) (QUOTE NIL) (QUOTE REC))
84200 (PUTPROP (QUOTE VAR_VARNOT) (QUOTE NIL) (QUOTE ASSUM))
84300 (PUTPROP (QUOTE VAR_VARNOT) (QUOTE (V3 V9 T1 T2)) (QUOTE ARG))
84400 (PUTPROP (QUOTE VAR_VARNOT) T (QUOTE OP))
84500 (PUTPROP (QUOTE VARVAR) (QUOTE NIL) (QUOTE INEQ))
84600 (PUTPROP (QUOTE VARVAR) (QUOTE NIL) (QUOTE REC))
84700 (PUTPROP (QUOTE VARVAR) (QUOTE NIL) (QUOTE ASSUM))
84800 (PUTPROP (QUOTE VARVAR) (QUOTE (V3 V9 T1 T2)) (QUOTE ARG))
84900 (PUTPROP (QUOTE VARVAR) T (QUOTE OP))
85000 (PUTPROP (QUOTE TUNIFY) (QUOTE NIL) (QUOTE INEQ))
85100 (PUTPROP (QUOTE TUNIFY) (QUOTE NIL) (QUOTE REC))
85200 (PUTPROP (QUOTE TUNIFY) (QUOTE NIL) (QUOTE ASSUM))
85300 (PUTPROP (QUOTE TUNIFY) (QUOTE NIL) (QUOTE ARG))
85400 (PUTPROP (QUOTE TUNIFY) T (QUOTE ITER))
85500 (PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE INEQ))
85600 (PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE REC))
85700 (PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE ASSUM))
85800 (PUTPROP (QUOTE ←) (QUOTE (V1 A1)) (QUOTE ARG))
85900 (PUTPROP (QUOTE ←) T (QUOTE OP))))
86000 EXPR)